Lambda the Ultimate

Hi,

Is it possible/plausible to have a Java/C++ like language in which you can write code like:

void aFunction(nonnull Object o) ....

Something s = new Something();
aFunction(s);

and then have the type system prove that o can never be null? This feels simple but I wonder if it ends up becoming dependent types, arbitrary theorem proving or some other suitably scary thing. Being able to add simple, small increases in type safety to a program written in a non-functional language would be quite nice to have!

I also wonder if this sort of thing could be implemented using C++ smart pointers.

"A preview of LINQ, code name for a set of extensions to the .NET Framework that encompass language-integrated data query, set, and transform operations."

First, thanks all to those responded to my post awhile ago. I picked a few brains and got some help, sorry if I didn't get a chance to write back to you.

So I am trying to make a very simple list oriented language (well more like preprocessor ala m4), I think there is a very "natural" solution (something that basically writes itself) to what I am looking for, but I was wondering if I could get some (more) help fleshing out the idea. Basically, I would just want to define list assignment, functions and function application over lists that is very \n delimiter oriented, with the default interpolation behaviour to take cross-products. This would be pseudo example, the idea being that the syntax would be very lightweight over a normal text file...

As->{
1
2
3
4
5
}

Bs->{
6
7
8
9
}

AsBs

>16
27
38
49
5

x-> is some number

6x

>6 is some number

6{1,2,3,4}

>61
62
63
64

level1a->{
A
AA
}

level1b->{
B
BB
}

level2->{
level1a level1a
level1a level1b
}

level2

>A A
A AA
AA A
AA AA
A B
A BB
AA B
AA BB

I am not sure exactly how well I've thought this out, but it gives you an idea...it's basically just subsitition with and emphasis on cross products that sacrifices some flexibility for simplicity by imposing things like new line delimiters. I would just need to be able to define lists function and apply them appropriately.

I can kinda see that by imposing newlines, I could swallow things one line at a time, but I keep thinking in terms of encoding an FSM with a bunch of "if" statements...

Should this be a peice of cake using something like recdescent? I would be cool if this was just basically something like a syntax modified perl, so that I could define functions with all the normal goodies.

Many thanks for any advice.

Hi i'm looking for literature and/or research on/in programming language design, implementation, etc, etc specifically in the domain of numerical analysis and scientific computing in general.

There seems to be a lack or slow down in development of array functional languages. From what i've investigated/researched already constraint-based programming is very well suited to numerical analysis problems and i can find alot of literature in that department.

I'm kind of curious of the possibility of a new language that is an array functional language which is purely functional, supports constraint-based programming, light-weight dependently typed type system, some kind of effects system in the type system for controlled, localized side-effects.

I know you probably think i'm crazy but i'm just curious :-)

I notice in stack based languages certain symmetric programs reduce to no-ops:

f1 = [swap swap] = []
f2 = [dup pop] = []
f3 = [cons uncons] = [] 
f4 = [dup swap cons uncons swap pop] = [dup swap swap pop] = [dup pop] = []

So how much of this is blindingly obvious to the research community? It seems that this must be much harder to detect in non stack based languages.

Cyclone is a type-safe dialect of C that incorporates a number of features from functional languages, including parametric polymorphism (ML-style, not C++), datatypes, and pattern matching. It also includes a number of features necessary to make C safe, such as fat pointers, tagged unions, and region-based memory management.

We've just put out a new release (1.0) and a new web site: http://cyclone.thelanguage.org

Even though I am not completely sure if LTU is the appropriate place to discuss this paper by Yves Guiraud, I see no danger in posting it anyway.

Abstract: In this document, we study a 3-polygraphic translation for the proofs of SKS, a formal system for classical propositional logic. We prove that the free 3-category generated by this 3-polygraph describes the proofs of classical propositional logic modulo structural bureaucracy. We give a 3-dimensional generalization of Penrose diagrams and use it to provide several pictures of a proof. We sketch how local transformations of proofs yield a non contrived example of 4-dimensional rewriting.

It discusses higher dimensional rewriting for SKS a deductive system for classical propositional logic in the style of the Calculus of Structures.
In intuitive sense this article has had a great appeal on me and I did not want to withhold it from the rest of us.

I consider myself an expert in imperative programming languages but I'm very green in the field of modern functional languages (I'd be better off alligator wrestling than writing monads, but I can still 'cadr' your 'cons'). Here is a quote from a well written post by Matt Helige ( http://lambda-the-ultimate.org/node/1455 ) which kept me up last night:

Things get more complicated (or is it simpler?) when you consider polymorphic types, like "α -> α" where α is a type variable rather than a concrete type. In a pure language with "parametric" polymorphism, there is only one function with this type. The word parametric in this context effectively means "type variables are black boxes": i.e., there's no way to say "if α = int, then..." or anything of that form. They're completely abstract. Once you see that, it's pretty easy to see that a type like α -> α can have only one implementation, or "inhabitant": since there is no conceivable way that the function can inspect its argument or construct a new value of the same (unknown) type, we can prove that any value with this type must be the identity function.

I didn't "see" what Matt was talking about until today. You have to realize that I think of C++ templates (and Java / C# generics) when I think about parameteric polymorphism. So I didn't understand where the restriction came from.

What had confused me was that in C++ the compiler does allow type choices by overloading template functions. Whether or not this is a "good thing" is probably debateable, so I figure why not debate it. Why or why not is C++ style parameterization where template T f(T x) {...} can legally have multiple implementations a good or bad thing?

The Fortress Language Spec v0.933

There is now a chapter on the memory model (Ch. 18).

Again, this spec looks more tidy than its predecessors.
Evaluation, types, and operators have their own chapters now.

Push 3.0 Language Description:

Push is a programming language intended primarily for use in evolutionary computation systems (such as genetic programming systems), as the language in which evolving programs are expressed. Push has an unusually simple syntax, which facilitates the development (or evolution) of mutation and recombination operators that generate and manipulate programs. Despite this simple syntax, Push provides more expressive power than most other program representations that are used for program evolution. Push programs can process multiple data types (without the syntax restrictions that usually accompany this capability), and they can express and make use of arbitrary control structures (e.g. recursive subroutines and macros) through the explicit manipulation of their own code (via a "CODE" data type). This allows Push to support the automatic evolution of modular program architectures in a particularly simple way, even when it Push is employed in an otherwise ordinary genetic programming system (such as PushGP, which is a "generic" GP system except that it evolves Push programs rather than Lisp-style program trees). Push can also support entirely new evolutionary computation paradigms such as "autoconstructive evolution," in which genetic operators and other components of the evolutionary system themselves evolve (as in the Pushpop and SwarmEvolve2 systems).